CoinductiveBuiltinList.agda:11,18-22
List A !=< ∞ (List A)
when checking that the expression _∷_ has type A → List A → List A
